propext {a b : Prop} : (a ↔ b) → a = b
propext {a b : Prop} : (a ↔ b) → a = b

命题外延性公理（propositional extensionality）的含义如下：它断言如果命题 a 和 b 逻辑等价（即我们能够从 b 推出 a，反之亦然）， 那么 a 和 b 是相等的，也就是说，在所有上下文中都可以用 b 替换掉 a。

对于像 a ∧ c ∨ d → e 这种简单表达式来说，我们可以直接证明，所有的逻辑运算符都保持逻辑等价，因此在这个表达式里，我们无需用 propext（命题外延）就可以把 a 替换为 b。 然而对于更高阶的表达式，如 P a，其中 P : Prop → Prop 是未知的，甚至对于 a = b 这种情形，都无法在没有一个明确声明此公理的前提下，把 a 替换为 b。

这是一个相对较无争议的公理，并且在直觉主义下是有效的。 然而, 当直接使用 #reduce 对证明进行化简时(这并不推荐), 这个公理会阻碍计算。 这意味着规范性(canonicity)——也就是所有类型为 Nat 的闭合项都归约成数字的性质——在使用这个(或任何)公理时将不再成立。

set_option pp.proofs true

def foo : Nat := by
  have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
  have := propext this ▸ (2 : Nat)
  exact this

#reduce foo
-- propext { mp := fun x x => True.intro, mpr := fun x => True.intro } ▸ 2

#eval foo -- 2

#eval可以将其计算为一个数值，因为编译器会消除类型转换并且不会计算证明，propext的返回类型是命题, 不会阻碍#evel的计算。